Nuprl Lemma : concat_append
0,22
postcript
pdf
ll1
,
ll2
:(Top List) List. concat(
ll1
@
ll2
) ~ (concat(
ll1
) @ concat(
ll2
))
latex
Definitions
concat(
ll
)
,
x
:
A
.
B
(
x
)
,
t
T
,
Top
Lemmas
top
wf
,
concat
wf
,
append
assoc
sq
origin
ll1, ll2:(Top List) List. concat(ll1 @ ll2) ~ (concat(ll1) @ concat(ll2)) ll1, ll2:(Top List) List. concat(ll1 @ ll2) ~ (concat(ll1) @ concat(ll2)) x:A. B(x)
T